<html>
<head><meta charset="utf-8"><title>Research topic · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html">Research topic</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="231434370"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231434370" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231434370">(Mar 23 2021 at 08:11)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> Hi. I've come across your PhD thesis and I am very impressed with it.  <br>
I am thinking about starting a PhD in a similar area (formal methods in Rust ), what would you suggest to be a good topic do drill into?<br>
Many thanks!</p>



<a name="231436087"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231436087" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231436087">(Mar 23 2021 at 08:29)</a>:</h4>
<p>A big open problem would be "compcert for rust." Compcert is a verified compiler for C in Coq.<br>
Another would be to verify the rust standard. Like what Robbert Krebbers' PhD-thesis for C.<br>
Unfortunately, rust does not seem to be standardized enough.</p>
<p>The conclusion of <span class="user-mention" data-user-id="120791">@RalfJ</span> 's paper is also interesting:<br>
<a href="https://cacm.acm.org/magazines/2021/4/251364-safe-systems-programming-in-rust/fulltext">https://cacm.acm.org/magazines/2021/4/251364-safe-systems-programming-in-rust/fulltext</a></p>
<blockquote>
<p>There is still much work left to do. Although RustBelt has recently been extended to account for the relaxed-memory concurrency model that Rust inherits from C++,9 there are a number of other Rust features and APIs that it does not yet cover, such as its "trait" system, which is complex enough to have been the source of subtle soundness bugs.7 Moreover, although verifying the soundness of an internally unsafe Rust library requires, at present, a deep background in formal semantics, we hope to eventually develop formal methods that can be put directly in the hands of programmers.</p>
</blockquote>
<blockquote>
<p>Finally, while RustBelt has focused on building foundations for Rust itself, we are pleased to see other research projects (notably Prusti6 and RustHorn27) beginning to explore an exciting, orthogonal direction: namely, the potential for Rust's strong type system to serve as a powerful tool in simplifying the formal verification of systems code.</p>
</blockquote>
<p><span class="user-mention" data-user-id="312719">@Xavier Denis</span> is making some progress in this direction, I think.</p>



<a name="231441613"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231441613" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231441613">(Mar 23 2021 at 09:24)</a>:</h4>
<p><span class="user-mention silent" data-user-id="382207">Bas Spitters</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231436087">said</a>:</p>
<blockquote>
<p>A big open problem would be "compcert for rust." Compcert is a verified compiler for C in Coq.<br>
Another would be to verify the rust standard. Like what Robbert Krebbers' PhD-thesis for C.<br>
Unfortunately, rust does not seem to be standardized enough.</p>
<p>The conclusion of <span class="user-mention silent" data-user-id="120791">RalfJ</span> 's paper is also interesting:<br>
<a href="https://cacm.acm.org/magazines/2021/4/251364-safe-systems-programming-in-rust/fulltext">https://cacm.acm.org/magazines/2021/4/251364-safe-systems-programming-in-rust/fulltext</a></p>
<blockquote>
<p>There is still much work left to do. Although RustBelt has recently been extended to account for the relaxed-memory concurrency model that Rust inherits from C++,9 there are a number of other Rust features and APIs that it does not yet cover, such as its "trait" system, which is complex enough to have been the source of subtle soundness bugs.7 Moreover, although verifying the soundness of an internally unsafe Rust library requires, at present, a deep background in formal semantics, we hope to eventually develop formal methods that can be put directly in the hands of programmers.</p>
</blockquote>
<blockquote>
<p>Finally, while RustBelt has focused on building foundations for Rust itself, we are pleased to see other research projects (notably Prusti6 and RustHorn27) beginning to explore an exciting, orthogonal direction: namely, the potential for Rust's strong type system to serve as a powerful tool in simplifying the formal verification of systems code.</p>
</blockquote>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> is making some progress in this direction, I think.</p>
</blockquote>
<p>Thanks. I know compcert  and it seems to be a quiet large effort for a PhD, but perhaps a subset of Rust might be a more reasonable target.</p>
<p>So it looks like there are two possible tangents, one being formal verification on written rust code like Prusti and Rust+F* project I have come across a some time ago. And the other being building foundations for Rust and the compiler itself.</p>



<a name="231444310"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231444310" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231444310">(Mar 23 2021 at 09:51)</a>:</h4>
<p>I don't think I've seen the rust+F* project.</p>
<p>A concrete project could be combing vellvm2 with wasmcert Coq. I don't know how difficult that would be.</p>



<a name="231447109"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231447109" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231447109">(Mar 23 2021 at 10:17)</a>:</h4>
<p>An alternative to compcert would be to do proof preserving compilation. The idea would be basically to take Rust code with Prusti/Creusot/LiquidRust annotations and compile it to, for example, RISC-5 assembly, which–as far as I know–has formal semantics, while also lowering the specifications. This way the only thing that would need to be part of the trusted codebase would be the checker that verifies the proof on the assembly level.</p>



<a name="231447506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231447506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231447506">(Mar 23 2021 at 10:20)</a>:</h4>
<p>Once Cranelift gets a RISC-V backend, I think using it as backend would be useful for this.</p>



<a name="231447592"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231447592" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231447592">(Mar 23 2021 at 10:21)</a>:</h4>
<p><span class="user-mention silent" data-user-id="133247">bjorn3</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231447506">said</a>:</p>
<blockquote>
<p>Once Cranelift gets a RISC-V backend, I think using it as backend would be useful for this.</p>
</blockquote>
<p>Any plans for Cranelift to get a RISC-5 backend?</p>



<a name="231447595"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231447595" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231447595">(Mar 23 2021 at 10:21)</a>:</h4>
<p>The Cranelift's regalloc has a check mode and there is already an informal proof for another component: <a href="https://github.com/bytecodealliance/wasmtime/blob/2880dab8f81249138b66528294df09eff45a935b/cranelift/codegen/src/machinst/buffer.rs#L155-L1476">https://github.com/bytecodealliance/wasmtime/blob/2880dab8f81249138b66528294df09eff45a935b/cranelift/codegen/src/machinst/buffer.rs#L155-L1476</a></p>



<a name="231447624"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231447624" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231447624">(Mar 23 2021 at 10:22)</a>:</h4>
<p><a href="https://github.com/bytecodealliance/wasmtime/issues/2217">https://github.com/bytecodealliance/wasmtime/issues/2217</a></p>



<a name="231447709"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231447709" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231447709">(Mar 23 2021 at 10:22)</a>:</h4>
<p>Nobody is actively working on it as far as I know though.</p>



<a name="231447736"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231447736" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231447736">(Mar 23 2021 at 10:22)</a>:</h4>
<p>Thanks for the update!</p>



<a name="231457651"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231457651" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231457651">(Mar 23 2021 at 11:55)</a>:</h4>
<p>Speaking of RISC-V. There's work on a verified compiler from bedrock2 to RISC-V. (Have a look at the IoT example!)<br>
<a href="https://github.com/mit-plv/bedrock2">https://github.com/mit-plv/bedrock2</a></p>
<blockquote>
<p>The source language is a "C-like" language called ExprImp. It is an imperative language with expressions. Currently, the only data type is word (32-bit or 64-bit), and the memory is a partial map from words to bytes. "Records" are supported as a notation for memory access with an offset.</p>
</blockquote>
<p>Making a formal connection between ExprImp and rust would be useful. I haven't looked closely enough at the differences.</p>



<a name="231458192"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231458192" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231458192">(Mar 23 2021 at 12:01)</a>:</h4>
<blockquote>
<p>It is a design decision to not support the following features:</p>
<ul>
<li>Function pointers</li>
<li>Recursive functions (we might add them later, but we always want to prove that we don't run out of stack space)</li>
<li>Non-terminating programs (except for the top-level event loop)</li>
</ul>
</blockquote>



<a name="231458350"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231458350" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231458350">(Mar 23 2021 at 12:02)</a>:</h4>
<p>In addition bedrock2 only supports storing words and not bytes in memory.</p>



<a name="231460257"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231460257" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231460257">(Mar 23 2021 at 12:20)</a>:</h4>
<p>bedrock2 is definitively much smaller than rust, but it may be a start, or inspiration, for a compiler of a subset of rust.<br>
Adam Chlipala is part of the risc-v committee, if I'm not mistaken.</p>



<a name="231506498"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231506498" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231506498">(Mar 23 2021 at 17:04)</a>:</h4>
<p><span class="user-mention" data-user-id="389506">@kentrixy</span> by Rust + F* do you mean HACSPEC?</p>



<a name="231506795"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231506795" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231506795">(Mar 23 2021 at 17:06)</a>:</h4>
<p>The approach that Vytautas described seems like it would be more tractable in the constraints of a PhD program than a verified compiler in Coq</p>



<a name="231507133"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231507133" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231507133">(Mar 23 2021 at 17:08)</a>:</h4>
<p>While a certified compiler is important for extremely high assurance software, I'm more concerned with verifying the functional correctness of Rust code, I think there are more low hanging fruits there</p>



<a name="231507183"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231507183" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231507183">(Mar 23 2021 at 17:08)</a>:</h4>
<p>Of course any sort of certified compilation for Rust would be super cool!</p>



<a name="231507622"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231507622" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231507622">(Mar 23 2021 at 17:11)</a>:</h4>
<p>There are plenty Rust verification topics that no one has attempted yet, it really depends on what your interests are</p>



<a name="231568712"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231568712" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231568712">(Mar 24 2021 at 01:19)</a>:</h4>
<p><span class="user-mention silent" data-user-id="382207">Bas Spitters</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231444310">said</a>:</p>
<blockquote>
<p>I don't think I've seen the rust+F* project.</p>
<p>A concrete project could be combing vellvm2 with wasmcert Coq. I don't know how difficult that would be.</p>
</blockquote>
<p>It is this PhD topic <a href="https://blog.merigoux.fr/en/2019/04/16/textinput.html">https://blog.merigoux.fr/en/2019/04/16/textinput.html</a></p>



<a name="231571101"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231571101" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231571101">(Mar 24 2021 at 01:54)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231507133">said</a>:</p>
<blockquote>
<p>While a certified compiler is important for extremely high assurance software, I'm more concerned with verifying the functional correctness of Rust code, I think there are more low hanging fruits there</p>
</blockquote>
<p>Do you mind elaborate on that a bit more? There has been a few projects around it but what are some examples of topic of interest?</p>
<p>Thanks.</p>



<a name="231571218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231571218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231571218">(Mar 24 2021 at 01:56)</a>:</h4>
<p>I have tried out Prusti and it seems like that are lot of unsupported Rust features.</p>



<a name="231573295"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231573295" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231573295">(Mar 24 2021 at 02:26)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231506498">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="389506">kentrixy</span> by Rust + F* do you mean HACSPEC?</p>
</blockquote>
<p>I believe you are the author of <a href="https://github.com/xldenis/creusot">https://github.com/xldenis/creusot</a> <span aria-label="+1" class="emoji emoji-1f44d" role="img" title="+1">:+1:</span>  Very nice project/concept</p>



<a name="231606244"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231606244" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231606244">(Mar 24 2021 at 09:46)</a>:</h4>
<p>Yep that's me! Plenty of work left to do :) If you're interested in Denis' work, check out: <a href="https://github.com/hacspec/hacspec">https://github.com/hacspec/hacspec</a> which is the most recent iteration of this F* / Rust work. </p>
<p>AS for your question: What I mean is that certifying compilation of Rust hunts down / eliminates <em>compiler</em> bugs, I'm more interested in hunting down bugs in the Rust code <em>itself</em>.</p>



<a name="231606703"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231606703" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231606703">(Mar 24 2021 at 09:50)</a>:</h4>
<p>There are plenty of topics to explore here, for example: unsafe code, traits, async. Within each of these you can go in the direction of formalizing those systems, ie: what RustBelt did for the type system, you can also look at verifying code involving those aspects, aka Prusti / Creusot / MIRAI. Both of these are important directions since for example, RustBelt helps provide the (theoretical) foundations on which we can build verification tools</p>



<a name="231606809"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231606809" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231606809">(Mar 24 2021 at 09:51)</a>:</h4>
<p>And though it may still be early for this, there are doubtlessly a bunch of theses that could be written on engineering a complex verified piece of Rust code (ie an OS kernel, etc...)</p>



<a name="231606929"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231606929" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231606929">(Mar 24 2021 at 09:53)</a>:</h4>
<p>It all depends on where you see yourself on the 'theory &lt;-&gt; implementation' spectrum and what your specific interests are</p>



<a name="231611958"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231611958" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231611958">(Mar 24 2021 at 10:32)</a>:</h4>
<p>On the hacspec slack there's more discussion about an INRIA project verifying the riot bootloader.</p>



<a name="231768718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231768718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231768718">(Mar 25 2021 at 09:23)</a>:</h4>
<p><span class="user-mention silent" data-user-id="389506">kentrixy</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231434370">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> Hi. I've come across your PhD thesis and I am very impressed with it.  <br>
I am thinking about starting a PhD in a similar area (formal methods in Rust ), what would you suggest to be a good topic do drill into?<br>
Many thanks!</p>
</blockquote>
<p>Thanks. :)<br>
As was already said by others in this thread, I think "formal verification of functional correctness of Rust programs" is a wide open space with lots of opportunities for interesting ideas -- and an important space, too. You mentioned Prusti and that is is fairly limited in features; that is certainly true and it'd be interesting to figure out how to do something Prusti-like for more of Rust (supporting at least <code>Vec::iter_mut</code> and maybe even more complicated borrowing patterns), or how to marry Prusti-like verification of safe code with (manual or automated) verification of unsafe code.</p>



<a name="231769034"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231769034" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231769034">(Mar 25 2021 at 09:26)</a>:</h4>
<p>Another big one would be working towards a proper formal semantics for (a reasonable subset of) Rust itself -- ideally directly in terms of the surface language. Probably this is best done via elaboration to a smaller language, maybe something MIR-like.</p>



<a name="231769152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231769152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231769152">(Mar 25 2021 at 09:27)</a>:</h4>
<p>Formalizing the trait system comes to my mind; this part of Rust has not been extensively studied formally so far and yet the entire language relies on coherence of the trait system. With upcoming extensions like specialization, it becomes harder and harder to ensure correctness and coherence of the trait system, so this would also be a good way to have direct impact on language development.</p>



<a name="231770845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231770845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231770845">(Mar 25 2021 at 09:42)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231769034">said</a>:</p>
<blockquote>
<p>Another big one would be working towards a proper formal semantics for (a reasonable subset of) Rust itself -- ideally directly in terms of the surface language. Probably this is best done via elaboration to a smaller language, maybe something MIR-like.</p>
</blockquote>
<p>This is one of the goals of Ferrocene. I believe one could compare their goal to developing a rust standard, similar to the C-standard. <span class="user-mention" data-user-id="228996">@Sabree Blackmon</span> or  <span class="user-mention" data-user-id="215333">@Florian Gilcher</span> might want to chime in.<br>
<a href="https://ferrous-systems.com/blog/ferrocene-update-three-the-road/">https://ferrous-systems.com/blog/ferrocene-update-three-the-road/</a></p>



<a name="231772703"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231772703" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231772703">(Mar 25 2021 at 09:56)</a>:</h4>
<p>Yeah I know of Ferrocene. :) Though to me a "proper formal spec" implies having something machine-readable such as a Coq definition, which is usually out-of-scope for these kinds of standardization efforts and left to researchers. ;)</p>



<a name="231782002"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231782002" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231782002">(Mar 25 2021 at 11:12)</a>:</h4>
<p>But Robbert could not have written his thesis without the C standard. He was always so happy with that telephone sized book on his desk :-) <br>
<a href="https://robbertkrebbers.nl/thesis.html">https://robbertkrebbers.nl/thesis.html</a></p>



<a name="231782302"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231782302" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231782302">(Mar 25 2021 at 11:14)</a>:</h4>
<p>I think Robbert would have suffered much less pain if the C standard was written with a proper formal spec in mind. ;)</p>



<a name="231783240"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231783240" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231783240">(Mar 25 2021 at 11:22)</a>:</h4>
<p>Agreed. Hacspec is a good start, I hope one can build on that.<br>
The Concordium company is using rust for smart contracts. We're working on extraction from Coq to rust, and hopefully that subset of smart contracts could be specified.<br>
E.g.<br>
<a href="https://docs.rs/concordium-std/0.4.1/concordium_std/">https://docs.rs/concordium-std/0.4.1/concordium_std/</a></p>



<a name="231785579"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231785579" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231785579">(Mar 25 2021 at 11:43)</a>:</h4>
<p>The WASM spec is an outstanding prose document which was clearly written "with formalization in mind". I wish more language specs were written like that one. I don't think formalization is strictly required to write a "formalization in mind" document that is about as precise, although it's even better if someone in the research community starts doing formalization while the spec is under construction so that small issues can be found while it's early enough to make changes easily.</p>



<a name="231785865"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231785865" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231785865">(Mar 25 2021 at 11:45)</a>:</h4>
<p>Yeah, wasm is amazingly well-done.</p>



<a name="231785900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231785900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231785900">(Mar 25 2021 at 11:45)</a>:</h4>
<p>However, specifying wasm is also orders of magnitude easier than specifying Rust. ;)</p>



<a name="231786121"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231786121" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231786121">(Mar 25 2021 at 11:47)</a>:</h4>
<p>Well, the formalization was done almost simultaneously with the wasm document, and it is also referenced in the document. <span class="user-mention" data-user-id="271719">@Mario Carneiro</span> do we have a lean version of this already ;-) <br>
<a href="https://github.com/WasmCert/WasmCert-Coq">https://github.com/WasmCert/WasmCert-Coq</a></p>



<a name="231786771"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231786771" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231786771">(Mar 25 2021 at 11:52)</a>:</h4>
<p>Heh. I started porting CompCert a few years ago, but I eventually dropped it when the original client decided to do other things. C is just not a great language for formalization.<br>
<a href="https://github.com/digama0/kremlin">https://github.com/digama0/kremlin</a></p>



<a name="231787076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231787076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231787076">(Mar 25 2021 at 11:55)</a>:</h4>
<p>Hoping that rust will be better...</p>



<a name="231891598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231891598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231891598">(Mar 25 2021 at 23:21)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231606929">said</a>:</p>
<blockquote>
<p>It all depends on where you see yourself on the 'theory &lt;-&gt; implementation' spectrum and what your specific interests are</p>
</blockquote>
<p>thanks. My interest lies mostly in the "implementation" or practical part (I came from a SE background)</p>



<a name="231922460"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/231922460" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> kentrixy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#231922460">(Mar 26 2021 at 06:58)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231769034">said</a>:</p>
<blockquote>
<p>Another big one would be working towards a proper formal semantics for (a reasonable subset of) Rust itself -- ideally directly in terms of the surface language. Probably this is best done via elaboration to a smaller language, maybe something MIR-like.</p>
</blockquote>
<p>Thanks for the reply. Would you think something similar to the scope of "stacked borrow" part of your thesis would be suitable for a master thesis? I feel like that is something I am more interested in. i.e make a contribution to the compiler</p>



<a name="232013383"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232013383" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232013383">(Mar 26 2021 at 18:40)</a>:</h4>
<p>Stacked Borrows would be a pretty good master thesis in my book, yeah. :D But note that there are formal proofs there, not "just" a compiler/Miri implementation.</p>



<a name="232013432"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232013432" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232013432">(Mar 26 2021 at 18:40)</a>:</h4>
<p>but ultimately this is up to your thesis advisor</p>



<a name="232249104"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232249104" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> pandaman <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232249104">(Mar 29 2021 at 10:53)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/231769152">said</a>:</p>
<blockquote>
<p>Formalizing the trait system comes to my mind; this part of Rust has not been extensively studied formally so far and yet the entire language relies on coherence of the trait system. With upcoming extensions like specialization, it becomes harder and harder to ensure correctness and coherence of the trait system, so this would also be a good way to have direct impact on language development.</p>
</blockquote>
<p>Can you elaborate on what "correctness and coherence of the trait system" mean? Is it something like proving that the orphan rules actually allow at most one impl?</p>



<a name="232305052"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232305052" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232305052">(Mar 29 2021 at 17:31)</a>:</h4>
<p>it also means ensuring that we can't write 'bad' instances that break the invariants of the Rust type system. If I recall correctly there was a problem with Pin where it was possible to write 'evil' impls which would do UB.</p>



<a name="232305127"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232305127" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232305127">(Mar 29 2021 at 17:31)</a>:</h4>
<p>I dont <em>think</em> that proving hte uniqueness of instances would be the hard part</p>



<a name="232305218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232305218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232305218">(Mar 29 2021 at 17:32)</a>:</h4>
<p>but then again specialization throws a wrinkle in that</p>



<a name="232308677"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232308677" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232308677">(Mar 29 2021 at 17:52)</a>:</h4>
<p>I think the hard part is just that there are so many moving parts and quite a lot of assumptions/requirements about how they need to fit together, none of which have been formally stated, much less proved</p>



<a name="232308758"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232308758" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232308758">(Mar 29 2021 at 17:53)</a>:</h4>
<p>I would very much like to see a formal (or informal) specification of the complete rust type system</p>



<a name="232308783"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232308783" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232308783">(Mar 29 2021 at 17:53)</a>:</h4>
<p>it's always bigger than you think at first</p>



<a name="232309812"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232309812" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232309812">(Mar 29 2021 at 18:00)</a>:</h4>
<p>yep! i really think that writing down the rust trait system, how it chooses to resolve instances etc would be huge already</p>



<a name="232309825"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232309825" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232309825">(Mar 29 2021 at 18:00)</a>:</h4>
<p>and a huge amount of work</p>



<a name="232921324"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232921324" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232921324">(Apr 02 2021 at 16:43)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/232305052">said</a>:</p>
<blockquote>
<p>it also means ensuring that we can't write 'bad' instances that break the invariants of the Rust type system. If I recall correctly there was a problem with Pin where it was possible to write 'evil' impls which would do UB.</p>
</blockquote>
<p>this is "hard mode" where you don't just have to show coherence of the trait system but then have to find a way for unsafe code to <em>exploit</em> coherence of the trait system</p>



<a name="232921415"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/232921415" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#232921415">(Apr 02 2021 at 16:44)</a>:</h4>
<blockquote>
<p>Is it something like proving that the orphan rules actually allow at most one impl?</p>
</blockquote>
<p>That's the core of it, yes -- most trait system unsoundnesses boil down to coherence issues I think</p>



<a name="233080070"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/233080070" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#233080070">(Apr 04 2021 at 13:05)</a>:</h4>
<p>Yea I figure there are some particular issues due to ‘fundamental’ types which could be interesting to reason about</p>



<a name="233776171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/233776171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#233776171">(Apr 09 2021 at 06:58)</a>:</h4>
<p>About formalizing the trait system, it would already be useful to do this for the hacspec subset of rust. Trait are used quite a bit in the cryptographic libraries. hacspec has a clear operational semantics.</p>



<a name="235843772"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235843772" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235843772">(Apr 23 2021 at 13:53)</a>:</h4>
<p>Regarding formalizing the trait system, it's worth pointing out that this work is already well underway in <a href="https://rust-lang.github.io/chalk/book/">chalk</a> -- as well as an effort to put that formalization into practice as the basis for the compiler and rust-analyzer.</p>



<a name="235843824"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235843824" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235843824">(Apr 23 2021 at 13:53)</a>:</h4>
<p>That work is coordinated in <a class="stream" data-stream-id="144729" href="/#narrow/stream/144729-wg-traits">#wg-traits</a></p>



<a name="235843895"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235843895" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235843895">(Apr 23 2021 at 13:54)</a>:</h4>
<p>Similarly, <a href="https://github.com/rust-lang/polonius/">polonius</a> includes the basis for a formal specification of the borrow checker; that work is generally coordinated in <a class="stream" data-stream-id="186049" href="/#narrow/stream/186049-t-compiler.2Fwg-polonius">#t-compiler/wg-polonius</a></p>



<a name="235844031"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235844031" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235844031">(Apr 23 2021 at 13:55)</a>:</h4>
<p>I think what would be interesting, besides pursuing and elaborating those projects, is trying to stitch them together with a formalization of the <a href="https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir/src/borrow_check/type_check/mod.rs">MIR type checker</a>, which would then be a complete type system for MIR.</p>



<a name="235844074"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235844074" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235844074">(Apr 23 2021 at 13:55)</a>:</h4>
<p>I don't think it's worth even thinking about a formal spec or type system for surface rust syntax at this stage.</p>



<a name="235852049"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235852049" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235852049">(Apr 23 2021 at 14:43)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> Is there an overview of the difference between the MIR type checker and rustbelt?</p>



<a name="235857451"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235857451" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235857451">(Apr 23 2021 at 15:10)</a>:</h4>
<p>The MIR type checker can't be used to do any formal verification. It only checks if the program is well-typed. It doesn't check that the program doesn't panic or contains functions with <code>unsafe</code> blocks that are unsound.</p>



<a name="235857848"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235857848" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235857848">(Apr 23 2021 at 15:11)</a>:</h4>
<p><span class="user-mention silent" data-user-id="382207">Bas Spitters</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/235852049">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> Is there an overview of the difference between the MIR type checker and rustbelt?</p>
</blockquote>
<p>I don't think we have a list. In terms of borrow checking, RustBelt's typing rules were defined before NLL was solidified so it is more "inspired by" the real thing than closely modeling it. the main differences I am aware of are</p>
<ul>
<li>RustBelt doesn't have two-phase borrows</li>
<li>RustBelt doesn't support code that reads from a <code>&amp;mut</code> with an outstanding shared loan (I simply was not aware that rustc allows this^^)</li>
</ul>
<p>Outside borrow checking and traits there's not a lot happening that is very interesting, is it? RustBelt does "move tracking" in linear type system style; I am not sure if whatever strategy rustc uses has been formalized.</p>



<a name="235857997"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235857997" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235857997">(Apr 23 2021 at 15:12)</a>:</h4>
<p><span class="user-mention silent" data-user-id="133247">bjorn3</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/235857451">said</a>:</p>
<blockquote>
<p>The MIR type checker can't be used to do any formal verification. It only checks if the program is well-typed. It doesn't check that the program doesn't panic or contains functions with <code>unsafe</code> blocks that are unsound.</p>
</blockquote>
<p>well-typed is still a very interesting property.^^</p>



<a name="235858123"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235858123" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235858123">(Apr 23 2021 at 15:12)</a>:</h4>
<p>I think that there are three parts to formalizing Rust traits:<br>
1) What does the trait part of the typesystem mean: what is allowed, what is not allowed, how is the instance selected, is it coherent, etc.<br>
2) What are the properties of a given trait.<br>
    eg a formal statement of what a FusedIterator is required to do.<br>
    (I was going to give examples involving whether Add and Mul are commutative, associative and distributive - but the answer would sadly have to be "no")<br>
3) Proving that instances actually satisfy any properties that they are meant to satisfy.</p>



<a name="235858944"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235858944" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235858944">(Apr 23 2021 at 15:15)</a>:</h4>
<p>A few things that come to mind: drop checking, more primitives (async/yield?), intrinsics / "boring" things that make the difference between production compiler and research MVP</p>



<a name="235859083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235859083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235859083">(Apr 23 2021 at 15:15)</a>:</h4>
<p>I would assume that for an actual mir typechecker you need all the boring things</p>



<a name="235859298"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235859298" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235859298">(Apr 23 2021 at 15:16)</a>:</h4>
<p>I don't have a good sense of how the type system and traits differ between surface rust and MIR</p>



<a name="235859461"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235859461" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235859461">(Apr 23 2021 at 15:17)</a>:</h4>
<p>I don't think there is any difference for the type system itself.</p>



<a name="235859738"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235859738" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235859738">(Apr 23 2021 at 15:19)</a>:</h4>
<p>The fact that traits can contain associated types, that traits and wellformedness can appear inductively and coinductively in chalk suggests that the actual semantic model for traits might be quite subtle; it seems like it brushes up against some inconsistent logical systems</p>



<a name="235860100"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235860100" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235860100">(Apr 23 2021 at 15:21)</a>:</h4>
<p>Oh, const eval is another big missing part of formalizing the type system. This is still evolving, but min_const_generics is already stable</p>



<a name="235860983"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235860983" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235860983">(Apr 23 2021 at 15:27)</a>:</h4>
<p><span class="user-mention" data-user-id="271719">@Mario Carneiro</span> Your list of boring things includes intrinsics. It turns out that these are equally necessary and equally boring for verification tools, static analysis tools, etc. And, in the case of SIMD intrinsics, it is relatively easy (but fairly tedious) to write an emulation library that implements all of the SIMD intrinsics needed.<br>
I have done this for use with KLEE (code: <a href="https://github.com/project-oak/rust-verification-tools/tree/main/simd_emulation">https://github.com/project-oak/rust-verification-tools/tree/main/simd_emulation</a>) and the code should be usable by other tools. For my usage, it turns out that I only need a small number of intrinsics because I go via LLVM and LLVM is able to lower most of the SIMD intrinsics that are not processor specific. More would probably be needed to support tools that work at the MIR level.<br>
I'm happy to help if others want to work on a shared SIMD emulation library - to make it work with more tools, to add tests, to increase the number of intrinsics, etc.</p>



<a name="235920743"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235920743" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235920743">(Apr 23 2021 at 22:58)</a>:</h4>
<p><span class="user-mention silent" data-user-id="336739">Alastair Reid</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/235858123">said</a>:</p>
<blockquote>
<p>2) What are the properties of a given trait.<br>
    eg a formal statement of what a FusedIterator is required to do.<br>
    (I was going to give examples involving whether Add and Mul are commutative, associative and distributive - but the answer would sadly have to be "no")</p>
</blockquote>
<p>This is an interesting item to include. If the trait is not declared <code>unsafe</code>, I don't think it should be required -- or perhaps it's a question of having distinct goals in mind.</p>



<a name="235920898"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235920898" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235920898">(Apr 23 2021 at 22:59)</a>:</h4>
<p>If the goal is proving functional correctness, and you are relying on impls proving that they implement some protocol defined by the trait, than it makes sense. It may suggest either having a distinct kind of "trait proof" (one that considers a subset of impls that are themselves proven to meet defined bounds) or other interesting criteria.</p>



<a name="235920908"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235920908" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235920908">(Apr 23 2021 at 22:59)</a>:</h4>
<p>I guess we could imagine generalizing <code>unsafe</code> to "something impls must prove to be legal"</p>



<a name="235920983"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235920983" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235920983">(Apr 23 2021 at 23:00)</a>:</h4>
<p><span class="user-mention silent" data-user-id="336739">Alastair Reid</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Research.20topic/near/235858123">said</a>:</p>
<blockquote>
<p>1) What does the trait part of the typesystem mean: what is allowed, what is not allowed, how is the instance selected, is it coherent, etc.</p>
</blockquote>
<p>This is what chalk is focused on.</p>



<a name="235958887"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235958887" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235958887">(Apr 24 2021 at 10:06)</a>:</h4>
<blockquote>
<p>This is an interesting item to include. If the trait is not declared unsafe, I don't think it should be required -- or perhaps it's a question of having distinct goals in mind.</p>
</blockquote>
<p>even for safe traits, such contracts will be relevant when verifying functional correctness<br>
(as you said later)</p>



<a name="235967055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/235967055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#235967055">(Apr 24 2021 at 12:34)</a>:</h4>
<p>(yes, agreed)</p>



<a name="236079352"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Research%20topic/near/236079352" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Michael George <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Research.20topic.html#236079352">(Apr 25 2021 at 17:07)</a>:</h4>
<p>Incidentally, I've just started a project to learn rust, and it happens to be a design for traits for describing the properties of add, mul, etc: <a href="https://github.com/mdgeorge4153/rusted-roots">https://github.com/mdgeorge4153/rusted-roots</a>.  It might be a good test case for traits for functional correctness</p>
<p>It's not very complete or well written, really just a sketch while I'm learning my way around rust</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>